Skip to content

feat(Geometry/Curve): add Frenet–Serret framework#38348

Open
mirajcs wants to merge 17 commits intoleanprover-community:masterfrom
mirajcs:curves
Open

feat(Geometry/Curve): add Frenet–Serret framework#38348
mirajcs wants to merge 17 commits intoleanprover-community:masterfrom
mirajcs:curves

Conversation

@mirajcs
Copy link
Copy Markdown

@mirajcs mirajcs commented Apr 21, 2026

This PR introduces a basic formalization of smooth parametrized curves in ℝ³
(EuclideanSpace ℝ (Fin 3)) together with the Frenet frame and partial proofs
of the Frenet–Serret formulas.

Main contributions:

  • Define ParametrizedDifferentiableCurve as a smooth map on an open interval.
  • Define arc length and arc-length parametrization.
  • Define geometric quantities:
    • curvature κ(t) = ‖α''(t)‖
    • tangent, normal, and binormal vector fields
    • torsion via ‖B'(t)‖
  • Introduce the FrenetFrame structure.
  • Prove key Frenet–Serret formulas:
    • T' = κ • N
    • B' = -τ • N
    • N' = -κ • T + τ • B

The implementation relies on existing analysis and inner product space
infrastructure, as well as properties of the cross product in ℝ³.
Some intermediate lemmas about orthogonality and cross-product identities
are included.

At present, some results assume nonvanishing curvature/torsion and include
auxiliary hypotheses about derivatives. These can be streamlined in future work.

This development is intended as a foundation for further formalization of
classical differential geometry (curves and surfaces).

@github-actions github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Apr 21, 2026
@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 21, 2026

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 21, 2026 •
edited
Loading

PR summary c63c4e5c93

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Geometry.Curves.Basic (new file) 2426

Declarations diff

+ Curvature3
+ FrenetFrame
+ FrenetSerretFrameVectorsExistence
+ ParametrizedDifferentiableCurve
+ ParametrizedDifferentiableCurve3
+ Torsion3
+ arcLength
+ arcLength3
+ binormal_cross
+ curveBinormal3
+ curveNormal3
+ curveTangent3
+ derivBinormal
+ derivTangent
+ deriv_normal
+ dot_tangent
+ frenetTrihedron
+ gsFrenetFrame
+ gsFrenetFrame_orthonormal
+ isArcLengthParametrized
+ isArcLengthParametrized3
+ orthogonality_tangent_normal
+ rawFrenetVecs
+ regularCurve
+ regularCurve3

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

⚠️ Workflow documentation reminder

This PR modifies files under .github/workflows/.
Please update docs/workflows.md if the workflow inventory, triggers, or behavior changed.

Modified workflow files:

  • .github/workflows/build_template.yml

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 21, 2026 •
edited
Loading

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

@mirajcs mirajcs changed the title Add Frenet–Serret framework for parametrized curves in ℝ³ feat(Geometry/Curve): add Frenet–Serret framework Apr 21, 2026
@mirajcs
Copy link
Copy Markdown
Author

mirajcs commented Apr 22, 2026

Ready for review. All CI checks are passing.

@vihdzp
Copy link
Copy Markdown
Collaborator

vihdzp commented Apr 22, 2026

a) There seems to be a generalization of this to finitely many dimensions. Could we develop this instead, and get the case dim = 3 as a special case if need be?
b) Was any of this written by AI?

@vihdzp vihdzp added the t-differential-geometry Manifolds etc label Apr 22, 2026
@mirajcs
Copy link
Copy Markdown
Author

mirajcs commented Apr 22, 2026

@vihdzp Thanks for the feedback!

a) That’s a good point. I focused on the 3-dimensional case to keep the development concrete, but I agree that a formulation in arbitrary finite dimensions would be more natural. I believe this should go through an alternating multilinear construction (or equivalently via a Hodge-star-type operator), so that the 3D cross product appears as a special case. I’ll look into whether the current development can be refactored along these lines and whether this generalization fits well with existing mathlib abstractions.

b) I did not generate the code with AI. I have used AI tools occasionally to explore tactics or get ideas, but all code has been written and verified by me.

@vihdzp
Copy link
Copy Markdown
Collaborator

vihdzp commented Apr 22, 2026

The Hodge star is a longstanding TODO... that by itself would be a good project.

@sgouezel sgouezel removed their assignment Apr 26, 2026
wwylele
wwylele reviewed Apr 26, 2026
View reviewed changes
Comment thread .github/workflows/build_template.yml
Comment on lines +771 to +776
- name: Configure Lean
uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0
with:
auto-config: false
use-github-cache: false
use-mathlib-cache: false
Copy link
Copy Markdown
Collaborator

@wwylele wwylele Apr 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please don't make changes to CI in an unrelated PR.

Copy link
Copy Markdown
Author

@mirajcs mirajcs Apr 27, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for pointing that out. I apologize for modifying the CI configuration in an unrelated PR, that was not intentional. I’ll make sure to keep such changes separate and scoped appropriately in the future.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@wwylele wwylele wwylele left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-differential-geometry Manifolds etc

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@mirajcs @vihdzp @wwylele @sgouezel